package tableaux;

import java.util.Collection;
//import java.util.HashMap;
//import java.util.Collections;
import java.util.HashSet;
import java.util.LinkedList;
//import java.util.Map;
import java.util.Set;
import java.util.Stack;

import option.InitParam;

import preprocessor.absorption.Absorption;

//import preprocessor.Simplification;
//import preprocessor.absorption.extended.AssertionConversion;
import reasoner.care.TestEval;
import tableaux.backjumping.Backjumping;
import tableaux.backjumping.DependencyImp;
import tableaux.backjumping.DependencyImpMax;
import tableaux.rules.*;
import utils.Display;
import utils.exception.BackjumpingNoDepSetException;

import entities.Individual;
import entities.assertion.Assertion;
import entities.assertion.ConceptAssertion;
import entities.concept.*;
import kb.*;

public class Completion {
	public static final boolean DEP_MAX = InitParam
			.getBooleanProperty("backjumping.max");

	public static final boolean fullyGuardedReasoning = InitParam
			.getBooleanProperty("reasoning.guarding.full");
	public static final boolean partiallyGuardedReasoning = fullyGuardedReasoning
			|| InitParam.getBooleanProperty("reasoning.guarding.partial");
	public static final boolean MergeNominal = InitParam
			.getBooleanProperty("reasoning.guarding.nominal.merge");
	// if true, feature guards are introduced in a rule, otherwise they are
	// added as GCIs
	public static final boolean featureGuardsInRule = fullyGuardedReasoning
			&& InitParam.getBooleanProperty("reasoning.guarding.feature.rule");
//	// if as a rule, Forall R.C always introduce DEF_r
//	public static final boolean universalGuardsInRule = partiallyGuardedReasoning
//			&& InitParam
//					.getBooleanProperty("reasoning.guarding.universal.rule");

	public static boolean nominalInTu = Absorption.NCA && false;

	private TBox tb;
	private ABox ab;
	private InitGraph dg;
	private Assertion ast;
	private Branching currentBranch;
	private Stack<Branching> allBranchesInPath;

	public Stack<Branching> getAllBranchesInPath() {
		return allBranchesInPath;
	}

	// private LinkedList<Individual> individualsInQueue;
	//
	// public LinkedList<Individual> getIndividualsInQueue() {
	// return individualsInQueue;
	// }

	private Set<Individual> individualsInQueue;

	public Set<Individual> getIndividualsInQueue() {
		return individualsInQueue;
	}

	private ClashTrigger clashtrigger;

	private void init() {
		this.currentBranch = null;
		this.allBranchesInPath = new Stack<Branching>();
		// this.individualsInQueue = new LinkedList<Individual>();
		this.individualsInQueue = new HashSet<Individual>();
	}

	/**
	 * when the parameter assertion is null, this checks the consistency of the
	 * ABox
	 * 
	 * @param tb
	 * @param ab
	 * @param c
	 * @param as
	 */
	public Completion(TBox tb, ABox ab, Assertion as) {
		init();
		if (tb == null) {
			tb = new TBox();
		}
		if (ab == null) {
			ab = new ABox();
		}
		this.tb = tb;
		this.ab = ab;
		this.ast = as;
		this.clashtrigger = new ClashTrigger(this.tb);
	}

	// for any a:C, add DEF_a, DEF_f for any f in C
	// private Set<Concept> initQuery(Nominal o, Concept c){
	// Set<Concept> ret = new HashSet<Concept>();
	// PConcept defa = PConcept.newGuardPConcept(o);
	// ret.add(defa);
	// // for(Role f:c.extractFeatures()){
	// // ret.add(PConcept.newGuardPConcept(f));
	// // }
	// // //temporary mod
	// // for(Role r:c.extractRoles()){
	// // ret.add(PConcept.newGuardPConcept(r));
	// // }
	// return ret;
	// }

	private void initRoot() {
		if (partiallyGuardedReasoning) {
			// guarded reasoning
			if (ast != null && ast instanceof ConceptAssertion) {
				ConceptAssertion ca = ast.asConceptAssertion();
				Individual initNode = Individual.getAnonIndividual();
				initNode.setAsTableauRoot();
				// Individual initNode = ca.getIndividual();
				Concept deri = DerivativeConcept.generateFromAssertion(ca,
						initNode, this.tb);
				if (initNode.addLabels(deri)
						&& this.getCurrentBranching() != null) {
					if (BranchChanges.getRecordingStatus()) {
						this.currentBranch.getBranchChanges().addToLabel(
								initNode, deri);
					}
				}
				this.individualsInQueue.add(initNode);
			}
		} else {
			// ordinary reasoning
			this.dg = new InitGraph(this, ab);
			this.dg.ABox2DataGraph();
			if (ast != null && ast instanceof ConceptAssertion) {
				ConceptAssertion ca = ast.asConceptAssertion();
				this.individualsInQueue.add(ca.getIndividual());
				Concept c = preprocessor.Simplification.NNF(ca.getConcept(),
						false);
				ast = new ConceptAssertion(ca.getIndividual(), c);
				this.dg.addNewAssertion(ast);
			}
		}

	}

	/**
	 * 
	 * check if A is consistent. Input: always a:C with Tb and Ab. Ab is empty
	 * for guarded reasoning. For c -> d w.r.t. empty theory. For K U a:C |=
	 * b:D, the input is: the LHS is converted into Tb, the RHS will be b:~D.
	 * 
	 * @return
	 */
	public boolean checkABoxConsistency() {
		RuleExists.print = false;
		boolean cons = false;
		this.initRoot();
		if (individualsInQueue == null || individualsInQueue.size() < 1) {
			return true;
		}
		if (!Completion.partiallyGuardedReasoning) {
			// if no guarded reasoning, add all instances
			this.individualsInQueue.addAll(ab.getABoxIndividuals());
			// System.out.println("All individuals added: "+this.individualsInQueue.size());
		}
		// Individual root = this.individualsInQueue.getFirst();
		Individual root = this.individualsInQueue.iterator().next();
		BranchChanges.setRecordingStatus(false);
		// clear dependencies
		if (Completion.DEP_MAX) {
			DependencyImpMax.clearDependencies();
		} else {
			DependencyImp.clearDependencies();
		}
		if (clashtrigger.clashFound(root)) {
			root.setSat(false);
			cons = false;
			this.individualsInQueue.clear();
			return cons;
		}
//		 if(root.getLabels().toString().contains(Display.NOMINAL_LEFT_SIGN
//				 +"http://www.Department0.University0.edu/GraduateStudent0"+Display.NOMINAL_RIGHT_SIGN)){
//			 System.out.println("testing:" +root+"\n"+root.getLabels());
//			 RuleExists.print = true;
//		 }
		// start processing the individual queue
		while (!this.individualsInQueue.isEmpty()) {
			Individual expind = selectNextIndToExpand(IndExpansionOrder.CLASH_FIRST);
			if (expind.isBlocked()) {
				boolean rmed = this.removeIndividualFromQueue(expind);
				if (rmed && BranchChanges.getRecordingStatus()) {
					this.currentBranch.getBranchChanges().updateQueueInds(
							expind, -1);
				}
				continue;
			}
			boolean initsat = this.expansion(expind);
			if (!initsat) {
				try {
					if (!new Backjumping(this).hasNextBranching(expind,
							clashtrigger.getClashingConcepts())) {
						// after expansion, remove all clashes if any.
						this.clashtrigger.clearClashes();
						//
						cons = false;
						expind.setSat(false);
						this.allBranchesInPath.clear();
						this.individualsInQueue.clear();
						return cons;
					} else {
						// after expansion, remove all clashes if any.
						this.clashtrigger.clearClashes();
						//
						continue;
					}
				} catch (BackjumpingNoDepSetException e) {
					e.printStackTrace();
				}
			} else {
				// after expansion, remove all clashes if any.
				this.clashtrigger.clearClashes();
				//
				cons = true;
				expind.setSat(true);
				boolean rmed = this.removeIndividualFromQueue(expind);
				if (rmed && BranchChanges.getRecordingStatus()) {
					this.currentBranch.getBranchChanges().updateQueueInds(
							expind, -1);
				}
				boolean clearstack = false;
				if (this.individualsInQueue.size() < 1) {
					clearstack = true;
				}
				// else{
				// for(Individual ind:this.individualsInQueue){
				// if(expind.hasThisAncestor(ind)){
				// clearstack = false;
				// break;
				// }
				// }
				// }
				// clear the stack of branches only if no other nodes will refer
				// to the stack
				if (clearstack) {
					this.allBranchesInPath.clear();
				}
			}

		}
		if (Thread.interrupted()) {
			System.err
					.println("\nThread interrupted: quitting CARE... \nResults may be incomplete... ");
			return cons;
		}
		return cons;
	}

	private enum IndExpansionOrder {
		HEAD_FIRST, CLASH_FIRST
	};

	private static int sizeRetriction = 15; // too large a queue requires too
											// many clash checks!

	private Individual selectNextIndToExpand(IndExpansionOrder expod) {
		switch (expod) {
		case HEAD_FIRST:
			// return this.individualsInQueue.peek();
			return this.individualsInQueue.iterator().next();
		case CLASH_FIRST:
			if (this.individualsInQueue.size() < sizeRetriction) {
				// for(int i=0; i<this.individualsInQueue.size(); i++){
				// Individual pot=this.individualsInQueue.get(i);
				// if(clashtrigger.clashFound(pot)){
				// return pot;
				// }
				// }
				for (Individual n : this.individualsInQueue) {
					if (clashtrigger.clashFound(n)) {
						return n;
					}
				}
			}
		default:
			// return this.individualsInQueue.peek();
			return this.individualsInQueue.iterator().next();
		}
	}

	public static void displayLabels(Collection<Individual> my) {
		// preserve the orders
		if (my instanceof LinkedList) {
			LinkedList<Individual> x = (LinkedList<Individual>) my;
			for (int i = 0; i < x.size(); i++) {
				System.out.println("index " + i + ", value: " + x.get(i)
						+ ", its order: " + x.get(i).getOrder());
			}
		} else {
			for (Individual ind : my) {
				System.out.println("====Display====\n\n" + ind.toString()
						+ " -> " + ind.getLabels());
			}
		}
	}

	// update all new nodes in this branch
	public void modifyQueueContent(Branching br) {
		br.getBranchChanges().recoverQueueInds(individualsInQueue);
		br.getBranchChanges().clearPotentialQueueInds();
	}

	private int ci = 0;

	public boolean expansion(Individual expind) {

		if (ci == 0) {
			TestEval.countOfTests++;
		}
		try {
			if (clashtrigger.clashFound(expind)) {
				return false;
			}
		} catch (Exception ex) {
			ex.printStackTrace();
		}
		boolean moreRules = true;
		boolean changed = false;
		boolean presat = true;
		boolean applied = false;
		while (!expind.isCompleted() && moreRules) {
			changed = false;
			applied = false;
			RuleNominal or = null;
			if (MergeNominal) {
				or = new RuleNominal(this);
			}
			RuleAnd cr = new RuleAnd(this);
			RuleOr dr = new RuleOr(this);
			RuleExists er = new RuleExists(this);
			RuleForAll fr = new RuleForAll(this);
			//
//			RuleForAllTrans trans = new RuleForAllTrans(this);
			//
			RuleLazyUnfolding ar = new RuleLazyUnfolding(this);
			// System.out.println("Testing node: "+expind.getOrder());
			if (MergeNominal && or.isApplicable(expind)) {
				changed |= or.applyRule(expind);
				applied = true;
			} else if (cr.isApplicable(expind)) {
				// System.out.println("Conjunction "+expind.getLabels());
				// TestEval.countOfAndExpansions ++;
				// long cur = System.currentTimeMillis();
				changed |= cr.applyRule(expind);
				// TestEval.countOfOrExpansionsTime +=
				// System.currentTimeMillis() - cur;
				applied = true;
			} else if (fr.isApplicable(expind)) {
				// System.out.println("For All "+expind.getLabels());
				changed |= fr.applyRule(expind);
				applied = true;
//			} else if (trans.isApplicable(expind)) {
//				// System.out.println("For All "+expind.getLabels());
//				changed |= trans.applyRule(expind);
//				applied = true;	
				
			} else if (ar.isApplicable(expind)) {
				// System.out.println("Lazy unfolding "+expind.getLabels());
				// more labels may be added to current node
				changed |= ar.applyRule(expind);
				applied = true;
			} else if (dr.isApplicable(expind)) {
				// System.out.println("Disjunction "+expind.getLabels());
				// add branching node to the queue, n is changed by adding a
				// branch label
				// TestEval.countOfOrExpansions ++;
				// long cur = System.currentTimeMillis();
				changed |= dr.applyRule(expind);
				// TestEval.countOfOrExpansionsTime +=
				// System.currentTimeMillis() - cur;
				applied = true;
			} else if (er.isApplicable(expind)) {
				// System.out.println("Exists "+expind.getLabels());
				// if changed is true, then the current node is modified by
				// adding the domain of the role!
				changed |= er.applyRule(expind);
				applied = true;
			}
			if (changed) {
				// if changed, the node has to be expanded again!
				presat = !clashtrigger.clashFound(expind);
				if (!presat) {
					return presat;
				}
			}
			// else if(!expind.moreRulesApplicable(this)){
			else if (!applied) {
				// not changed, no more rules
				// Set<Concept> explbs = new HashSet<Concept>();
				// explbs.addAll(expind.getExpandedLabels());
				// explbs.addAll(expind.getBinaryExpanded().keySet());
				// for(Set<AtomicConcept>
				// sc:expind.getBinaryExpanded().values()){
				// explbs.addAll(sc);
				// }
				// if(explbs.containsAll(expind.getLabels())){
				//
				// }
				moreRules = false;
				// expind.addBinaryToExpandedLabels();
				presat = !clashtrigger.clashFound(expind);
			}
		}
		return presat;
	}

	public Branching getCurrentBranching() {
		return this.currentBranch;
	}

	public InitGraph getCurrentDataGraph() {
		return this.dg;
	}

	public TBox getInitTBox() {
		return this.tb;
	}

	public ABox getInitABox() {
		return this.ab;
	}

	public static enum InQueueOrder {
		INQUEUEFIRST, INQUEUELAST
	};

	public boolean addToQueue(Individual n, InQueueOrder order) {
		// n.setAppliedGCI(false);
		if (this.individualsInQueue.contains(n)) {
			return false;
		}
		// if(order == InQueueOrder.INQUEUEFIRST){
		// this.individualsInQueue.addFirst(n);
		// }else if(order == InQueueOrder.INQUEUELAST){
		// this.individualsInQueue.addLast(n);
		// }
		this.individualsInQueue.add(n);
		return true;
	}

	public boolean removeIndividualFromQueue(Individual n) {
		if (!this.individualsInQueue.contains(n)) {
			return false;
		}
		this.individualsInQueue.remove(n);
		return true;
	}

	public void setCurrentBranch(Branching br) {
		if (this.currentBranch != null) {
			this.allBranchesInPath.push(this.currentBranch);
		}
		this.currentBranch = br;
	}

	public void replaceCurrentBranch(Branching br) {
		this.currentBranch = br;
	}

}
